- Add CLI parsing for --check-mode flag (full/validity/satisfiability)
- Remove deprecated --reach-check flag
- Update help message with check mode documentation
- Fix StrataVerify to use 'outcome' field instead of 'result'
- Update emoji symbols for better visual distinction:
  - ✅ for pass (valid and reachable)
  - ✔️ for always true if reachable
  - ✖️ for refuted if reachable
  - ❌ for refuted (always false and reachable)
  - ⛔ for unreachable
  - 🔶 for indecisive
  - ➕ for satisfiable
  - ➖ for reachable and can be false

- Add metadata fields: fullCheck, validityCheck, satisfiabilityCheck
- Add helper methods to check for these annotations
- Update verifySingleEnv to check metadata before using global checkMode
- Annotations override global --check-mode flag for specific statements

- Add VCOutcomeTests.lean with all 9 outcome combinations
- Test both predicate methods and emoji/label rendering
- Use named arguments for clarity
- Update SMTEncoderTests to use full check mode for existing tests
- Ensures backward compatibility with expected 'pass' outcome

- Add VCOutcomeTests.lean with all 9 outcome combinations
- Each test shows emoji and label in output for easy verification
- Use named arguments for clarity
- Update SMTEncoderTests to use full check mode for existing tests
- Ensures backward compatibility with expected 'pass' outcome

- Add VCOutcomeTests.lean with all 9 outcome combinations
- Use formatOutcome helper to avoid repetition
- Each test shows emoji and label in output
- Use named arguments for clarity
- Update SMTEncoderTests to use full check mode
- Ensures backward compatibility with expected 'pass' outcome

- Document CLI flag integration
- Document per-statement annotations
- Document emoji updates
- Document comprehensive test suite
- Document test fixes for backward compatibility

- Fix StrataVerify to properly format Except String VCOutcome
- Update StrataMain to use vcResult.outcome instead of vcResult.result
- Use isRefuted/isRefutedIfReachable predicates for failure detection
- Format outcomes with emoji and label

Clarifies that refuted outcome means reachable and always false

…ters

- Rename isRefuted -> isRefutedAndReachable
- Rename isIndecisive -> isIndecisiveAndReachable
- Rename isRefutedIfReachable -> isAlwaysFalseIfReachable
- Add backward compatibility aliases
- Add cross-cutting predicates: isAlwaysFalse, isAlwaysTrue, isReachable
- Enables filtering outcomes by properties across multiple cases

…ariants

- isPass: true if validityProperty is unsat (always true), regardless of reachability
- isPassAndReachable: true if (sat, unsat) - proven reachable and always true
- isPassIfReachable: true if (unknown, unsat) - always true if reachable
- Update label/emoji to use isPassAndReachable and isPassIfReachable
- Update test comments to reflect new naming
- Add backward compatibility alias isAlwaysTrueIfReachable

…overs all sat cases

- isSatisfiable: true for any sat satisfiabilityProperty
- isSatisfiableValidityUnknown: specific case (sat, unknown)
- Rename isPassIfReachable -> isPassReachabilityUnknown
- Rename isAlwaysFalseIfReachable -> isAlwaysFalseReachabilityUnknown
- Rename isReachableAndCanBeFalse -> isCanBeFalseAndReachable
- All predicates now have reachability info at the end
- Add backward compatibility aliases for all old names

- Nine base cases without 'is': passAndReachable, refutedAndReachable, etc.
- Derived predicates with 'is': isPass, isSatisfiable, isReachable, etc.
- Base cases represent exact outcome combinations
- Derived predicates check properties across multiple outcomes
- Update SarifOutput to use base cases in outcomeToLevel/outcomeToMessage
- Update label/emoji functions to use base cases
- Maintain backward compatibility aliases for all old names

- Add VerificationMode enum: deductive vs bugFinding
- Deductive mode: only pass is success, anything not proven is error/warning
- Bug finding mode: refuted is error, unknown is acceptable warning
- Group outcomes by severity (one .none, one .error, one .warning, one .note per mode)
- Default to deductive mode for backward compatibility

…e isAlwaysFalse

- Deductive mode: only pass/unreachable are success/note, everything else is error
- Bug finding mode: use isAlwaysFalse predicate instead of listing base cases
- Cleaner and more maintainable

…achable is warning in deductive

- Consistent naming: use 'alwaysFalse' instead of 'refuted' in base cases
- Deductive mode: unreachable is warning (dead code detection)
- Update all references in Verifier.lean and SarifOutput.lean
- Maintain backward compatibility aliases

- Replace isAlwaysFalse with explicit base cases: alwaysFalseAndReachable, alwaysFalseReachabilityUnknown
- Add comment listing all error cases in deductive mode
- Clearer mapping from base cases to severity levels

- Remove 'Verification succeeded/failed' language
- Use neutral descriptions: 'Always true and reachable', 'Always false and reachable'
- Messages work for any property type (assertion, invariant, requires, etc.)
- Shorter and clearer messages

…nknown outcomes

- alwaysFalseReachabilityUnknown has validityProperty = unknown (not sat), no counterexample
- unknown outcome can have models from either satisfiability or validity property
- Show models from both properties when available for unknown outcome

- alwaysFalseReachabilityUnknown has validityProperty = unknown (no model)
- unknown outcome also has no models (Result.unknown carries no data)
- Only Result.sat carries counterexample models

…rties

- Eliminates redundant predicate checks in outcomeToMessage
- Single exhaustive match covers all 9 base cases plus error cases
- More concise and easier to verify correctness

- Test predicates, messages, and severity levels for each outcome
- Verify deductive and bug finding modes produce correct SARIF levels
- Self-contained test outputs with no numbered comments
- Tests ensure SARIF output matches predicate semantics

- Add missing validityCheck parameter (now takes satisfiabilityCheck and validityCheck)
- Use Except.ok/Except.error to avoid ambiguity

… sat, val)

Addresses reviewer comment to use direct pattern matching instead of
nested boolean logic. Each case is now a single match arm.

…dant binding